package tr.edu.ege.kipler.satisfiability.syntactical;

import tr.edu.ege.kipler.syntax.BinaryBooleanExpression;
import tr.edu.ege.kipler.syntax.ModalExpression;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.WorldElementVisitor;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptDefinition;
import tr.edu.ege.kipler.syntax.atomicformula.ObjectRoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleInclusion;
import tr.edu.ege.kipler.syntax.atomicformula.SameIndividualAssertion;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class FormulaSimplificationVisitor implements WorldElementVisitor {
	private WorldElement normalForm;

	public WorldElement getNormalForm() {
		return normalForm;
	}

	public void visitBinaryElement(BinaryBooleanExpression be) {
		normalForm = be;
		FormulaSimplificationVisitor visitor = new FormulaSimplificationVisitor();
		be.getLhs().accept(visitor);
		be.setLhs(visitor.getNormalForm());
		visitor = new FormulaSimplificationVisitor();
		be.getRhs().accept(visitor);
		be.setRhs(visitor.getNormalForm());
	}

	public void visitConceptAssertion(ConceptAssertion ca) {
		normalForm = ca;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		ca.getConcept().accept(visitor);
		ca.setConcept(visitor.getNormalForm());
	}

	public void visitConceptDefinition(ConceptDefinition cd) {
		normalForm = cd;
		ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
		cd.getLhs().accept(visitor);
		cd.setLhs(visitor.getNormalForm());
		visitor = new ConceptSimplificationVisitor();
		cd.getRhs().accept(visitor);
		cd.setRhs(visitor.getNormalForm());
	}

	public void visitModalElement(ModalExpression me) {
		normalForm = me;
		FormulaSimplificationVisitor visitor = new FormulaSimplificationVisitor();
		me.getExpression().accept(visitor);
		me.setExpression(visitor.getNormalForm());
	}

	public void visitObjectRoleAssertion(ObjectRoleAssertion ra) {
		normalForm = ra;
	}

	public void visitRoleAssertion(RoleAssertion ra) {
		normalForm = ra;
	}

	public void visitRoleInclusion(RoleInclusion ri) {
		normalForm = ri;
	}

	public void visitSameIndividualAssertion(SameIndividualAssertion ia) {
		normalForm = ia;
	}

}
